

LEMMA

External connection implies connection.
=============================
Step 1

? (all x (all y ((ec x y) => (c x y))))


> revsk
=============================
Step 2

? ((~ (ec c586958 c586957)) v (c c586958 c586957))


> hypdisj
=============================
Step 3

? (c c586958 c586957)

1. (ec c586958 c586957)

> ((c X Y) <-- (ec X Y))
=============================
Step 4

? (ec c586958 c586957)

1. (~ (c c586958 c586957))
2. (ec c586958 c586957)

> hyp


LEMMA

Proper part implies parthood.
=============================
Step 1

? (all x (all y ((pp x y) => (p x y))))


> revsk
=============================
Step 2

? ((~ (pp c592087 c592086)) v (p c592087 c592086))


> hypdisj
=============================
Step 3

? (p c592087 c592086)

1. (pp c592087 c592086)

> ((p X Y) <-- (pp X Y))
=============================
Step 4

? (pp c592087 c592086)

1. (~ (p c592087 c592086))
2. (pp c592087 c592086)

> hyp


LEMMA

Tangential proper part implies proper part.
=============================
Step 1

? (all x (all y ((tpp x y) => (pp x y))))


> revsk
=============================
Step 2

? ((~ (tpp c597272 c597271)) v (pp c597272 c597271))


> hypdisj
=============================
Step 3

? (pp c597272 c597271)

1. (tpp c597272 c597271)

> ((pp X Y) <-- (tpp X Y))
=============================
Step 4

? (tpp c597272 c597271)

1. (~ (pp c597272 c597271))
2. (tpp c597272 c597271)

> hyp


LEMMA

Non-tangential proper part implies proper part.
=============================
Step 1

? (all x (all y ((ntpp x y) => (pp x y))))


> revsk
=============================
Step 2

? ((~ (ntpp c602513 c602512)) v (pp c602513 c602512))


> hypdisj
=============================
Step 3

? (pp c602513 c602512)

1. (ntpp c602513 c602512)

> ((pp X Y) <-- (ntpp X Y))
=============================
Step 4

? (ntpp c602513 c602512)

1. (~ (pp c602513 c602512))
2. (ntpp c602513 c602512)

> hyp


LEMMA

Parthood lifts connection from part to whole.
=============================
Step 1

? (all x (all y (all z (((p x y) & (c z x)) => (c z y)))))


> revsk
=============================
Step 2

? (((~ (p c607812 c607811)) v (~ (c c607810 c607812))) v (c c607810 c607811))


> hypdisj
=============================
Step 3

? (c c607810 c607811)

1. (c c607810 c607812)
2. (p c607812 c607811)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var24 c607811)
|
|1. (~ (c c607810 c607811))
|2. (c c607810 c607812)
|3. (p c607812 c607811)
|
|> hyp
=============================
Step 5

? (c c607810 c607812)

1. (~ (c c607810 c607811))
2. (c c607810 c607812)
3. (p c607812 c607811)

> hyp


LEMMA

If x is disconnected from y and y is a non-tangential proper part of z, then z is not part of x.
=============================
Step 1

? (all x (all y (all z (((dc x y) & (ntpp y z)) => (~ (p z x))))))


> revsk
=============================
Step 2

? (((~ (dc c613267 c613266)) v (~ (ntpp c613266 c613265))) v (~ (p c613265 c613267)))


> hypdisj
=============================
Step 3

? (~ (p c613265 c613267))

1. (ntpp c613266 c613265)
2. (dc c613267 c613266)

> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
|=============================
|Step 4
|
|? (c Var37 c613265)
|
|1. (p c613265 c613267)
|2. (ntpp c613266 c613265)
|3. (dc c613267 c613266)
|
|> ((c Y X) <-- (p Z X) (c Y Z))
||=============================
||Step 5
||
||? (p Var40 c613265)
||
||1. (~ (c Var37 c613265))
||2. (p c613265 c613267)
||3. (ntpp c613266 c613265)
||4. (dc c613267 c613266)
||
||> ((p X Y) <-- (pp X Y))
||=============================
||Step 6
||
||? (pp Var40 c613265)
||
||1. (~ (p Var40 c613265))
||2. (~ (c Var37 c613265))
||3. (p c613265 c613267)
||4. (ntpp c613266 c613265)
||5. (dc c613267 c613266)
||
||> ((pp X Y) <-- (ntpp X Y))
||=============================
||Step 7
||
||? (ntpp Var40 c613265)
||
||1. (~ (pp Var40 c613265))
||2. (~ (p Var40 c613265))
||3. (~ (c Var37 c613265))
||4. (p c613265 c613267)
||5. (ntpp c613266 c613265)
||6. (dc c613267 c613266)
||
||> hyp
|=============================
|Step 8
|
|? (c c613266 c613266)
|
|1. (~ (c c613266 c613265))
|2. (p c613265 c613267)
|3. (ntpp c613266 c613265)
|4. (dc c613267 c613266)
|
|> ((c X X) <--)
=============================
Step 9

? (~ (c c613266 c613267))

1. (p c613265 c613267)
2. (ntpp c613266 c613265)
3. (dc c613267 c613266)

> ((~ (c Y X)) <-- (~ (c X Y)))
=============================
Step 10

? (~ (c c613267 c613266))

1. (c c613266 c613267)
2. (p c613265 c613267)
3. (ntpp c613266 c613265)
4. (dc c613267 c613266)

> ((~ (c X Y)) <-- (dc X Y))
=============================
Step 11

? (dc c613267 c613266)

1. (c c613267 c613266)
2. (c c613266 c613267)
3. (p c613265 c613267)
4. (ntpp c613266 c613265)
5. (dc c613267 c613266)

> hyp


LEMMA

Case split on whether x is connected to z; if not, then dc x z.
=============================
Step 1

? (all x (all y (all z (((dc x y) & (ntpp y z)) => ((dc x z) v (c x z))))))


> revsk
=============================
Step 2

? (((~ (dc c618878 c618877)) v (~ (ntpp c618877 c618876))) v ((dc c618878 c618876) v (c c618878 c618876)))


> hypdisj
=============================
Step 3

? (c c618878 c618876)

1. (~ (dc c618878 c618876))
2. (ntpp c618877 c618876)
3. (dc c618878 c618877)

> ((c X Y) <-- (~ (dc X Y)))
=============================
Step 4

? (~ (dc c618878 c618876))

1. (~ (c c618878 c618876))
2. (~ (dc c618878 c618876))
3. (ntpp c618877 c618876)
4. (dc c618878 c618877)

> hyp


LEMMA

If x is connected to z, split on overlap to get ec x z or o x z.
=============================
Step 1

? (all x (all y (all z ((((dc x y) & (ntpp y z)) & (c x z)) => ((ec x z) v (o x z))))))


> revsk
=============================
Step 2

? ((((~ (dc c624755 c624754)) v (~ (ntpp c624754 c624753))) v (~ (c c624755 c624753))) v ((ec c624755 c624753) v (o c624755 c624753)))


> hypdisj
=============================
Step 3

? (o c624755 c624753)

1. (~ (ec c624755 c624753))
2. (c c624755 c624753)
3. (ntpp c624754 c624753)
4. (dc c624755 c624754)

> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|=============================
|Step 4
|
|? (c c624755 c624753)
|
|1. (~ (o c624755 c624753))
|2. (~ (ec c624755 c624753))
|3. (c c624755 c624753)
|4. (ntpp c624754 c624753)
|5. (dc c624755 c624754)
|
|> hyp
=============================
Step 5

? (~ (ec c624755 c624753))

1. (~ (o c624755 c624753))
2. (~ (ec c624755 c624753))
3. (c c624755 c624753)
4. (ntpp c624754 c624753)
5. (dc c624755 c624754)

> hyp


LEMMA

If x overlaps z and z is not part of x, then either po x z or pp x z.
=============================
Step 1

? (all x (all y (all z (((((dc x y) & (ntpp y z)) & (c x z)) & (o x z)) => ((po x z) v (pp x z))))))


> revsk
=============================
Step 2

? (((((~ (dc c631048 c631047)) v (~ (ntpp c631047 c631046))) v (~ (c c631048 c631046))) v (~ (o c631048 c631046))) v ((po c631048 c631046) v (pp c631048 c631046)))


> hypdisj
=============================
Step 3

? (pp c631048 c631046)

1. (~ (po c631048 c631046))
2. (o c631048 c631046)
3. (c c631048 c631046)
4. (ntpp c631047 c631046)
5. (dc c631048 c631047)

> ((pp Y X) <-- (p Y X) (~ (p X Y)))
|=============================
|Step 4
|
|? (p c631048 c631046)
|
|1. (~ (pp c631048 c631046))
|2. (~ (po c631048 c631046))
|3. (o c631048 c631046)
|4. (c c631048 c631046)
|5. (ntpp c631047 c631046)
|6. (dc c631048 c631047)
|
|> ((p Y X) <-- (p X Y) (~ (pp X Y)))
||=============================
||Step 5
||
||? (p c631046 c631048)
||
||1. (~ (p c631048 c631046))
||2. (~ (pp c631048 c631046))
||3. (~ (po c631048 c631046))
||4. (o c631048 c631046)
||5. (c c631048 c631046)
||6. (ntpp c631047 c631046)
||7. (dc c631048 c631047)
||
||> ((p Y X) <-- (o X Y) (~ (p X Y)) (~ (po X Y)))
||||=============================
||||Step 6
||||
||||? (o c631048 c631046)
||||
||||1. (~ (p c631046 c631048))
||||2. (~ (p c631048 c631046))
||||3. (~ (pp c631048 c631046))
||||4. (~ (po c631048 c631046))
||||5. (o c631048 c631046)
||||6. (c c631048 c631046)
||||7. (ntpp c631047 c631046)
||||8. (dc c631048 c631047)
||||
||||> hyp
|||=============================
|||Step 7
|||
|||? (~ (p c631048 c631046))
|||
|||1. (~ (p c631046 c631048))
|||2. (~ (p c631048 c631046))
|||3. (~ (pp c631048 c631046))
|||4. (~ (po c631048 c631046))
|||5. (o c631048 c631046)
|||6. (c c631048 c631046)
|||7. (ntpp c631047 c631046)
|||8. (dc c631048 c631047)
|||
|||> hyp
||=============================
||Step 8
||
||? (~ (po c631048 c631046))
||
||1. (~ (p c631046 c631048))
||2. (~ (p c631048 c631046))
||3. (~ (pp c631048 c631046))
||4. (~ (po c631048 c631046))
||5. (o c631048 c631046)
||6. (c c631048 c631046)
||7. (ntpp c631047 c631046)
||8. (dc c631048 c631047)
||
||> hyp
|=============================
|Step 9
|
|? (~ (pp c631046 c631048))
|
|1. (~ (p c631048 c631046))
|2. (~ (pp c631048 c631046))
|3. (~ (po c631048 c631046))
|4. (o c631048 c631046)
|5. (c c631048 c631046)
|6. (ntpp c631047 c631046)
|7. (dc c631048 c631047)
|
|> ((~ (pp X Y)) <-- (~ (p X Y)))
|=============================
|Step 10
|
|? (~ (p c631046 c631048))
|
|1. (pp c631046 c631048)
|2. (~ (p c631048 c631046))
|3. (~ (pp c631048 c631046))
|4. (~ (po c631048 c631046))
|5. (o c631048 c631046)
|6. (c c631048 c631046)
|7. (ntpp c631047 c631046)
|8. (dc c631048 c631047)
|
|> ((~ (p Z X)) <-- (dc X Y) (ntpp Y Z))
||=============================
||Step 11
||
||? (dc c631048 Var51)
||
||1. (p c631046 c631048)
||2. (pp c631046 c631048)
||3. (~ (p c631048 c631046))
||4. (~ (pp c631048 c631046))
||5. (~ (po c631048 c631046))
||6. (o c631048 c631046)
||7. (c c631048 c631046)
||8. (ntpp c631047 c631046)
||9. (dc c631048 c631047)
||
||> hyp
|=============================
|Step 12
|
|? (ntpp c631047 c631046)
|
|1. (p c631046 c631048)
|2. (pp c631046 c631048)
|3. (~ (p c631048 c631046))
|4. (~ (pp c631048 c631046))
|5. (~ (po c631048 c631046))
|6. (o c631048 c631046)
|7. (c c631048 c631046)
|8. (ntpp c631047 c631046)
|9. (dc c631048 c631047)
|
|> hyp
=============================
Step 13

? (~ (p c631046 c631048))

1. (~ (pp c631048 c631046))
2. (~ (po c631048 c631046))
3. (o c631048 c631046)
4. (c c631048 c631046)
5. (ntpp c631047 c631046)
6. (dc c631048 c631047)

> ((~ (p Z X)) <-- (dc X Y) (ntpp Y Z))
|=============================
|Step 14
|
|? (dc c631048 Var56)
|
|1. (p c631046 c631048)
|2. (~ (pp c631048 c631046))
|3. (~ (po c631048 c631046))
|4. (o c631048 c631046)
|5. (c c631048 c631046)
|6. (ntpp c631047 c631046)
|7. (dc c631048 c631047)
|
|> hyp
=============================
Step 15

? (ntpp c631047 c631046)

1. (p c631046 c631048)
2. (~ (pp c631048 c631046))
3. (~ (po c631048 c631046))
4. (o c631048 c631046)
5. (c c631048 c631046)
6. (ntpp c631047 c631046)
7. (dc c631048 c631047)

> hyp


LEMMA

Proper part decomposes into tangential or non-tangential proper part.
=============================
Step 1

? (all x (all y ((pp x y) => ((tpp x y) v (ntpp x y)))))


> revsk
=============================
Step 2

? ((~ (pp c637951 c637950)) v ((tpp c637951 c637950) v (ntpp c637951 c637950)))


> hypdisj
=============================
Step 3

? (ntpp c637951 c637950)

1. (~ (tpp c637951 c637950))
2. (pp c637951 c637950)

> ((ntpp Z X) <-- (pp Z X) (~ (ec (f631165 Z X Y) Z)))
|=============================
|Step 4
|
|? (pp c637951 c637950)
|
|1. (~ (ntpp c637951 c637950))
|2. (~ (tpp c637951 c637950))
|3. (pp c637951 c637950)
|
|> hyp
=============================
Step 5

? (~ (ec (f631165 c637951 c637950 Var32) c637951))

1. (~ (ntpp c637951 c637950))
2. (~ (tpp c637951 c637950))
3. (pp c637951 c637950)

> ((~ (ec X Y)) <-- (pp Y Z) (ec X Z) (~ (tpp Y Z)))
||=============================
||Step 6
||
||? (pp c637951 Var36)
||
||1. (ec (f631165 c637951 c637950 Var32) c637951)
||2. (~ (ntpp c637951 c637950))
||3. (~ (tpp c637951 c637950))
||4. (pp c637951 c637950)
||
||> hyp
|=============================
|Step 7
|
|? (ec (f631165 c637951 c637950 Var32) c637950)
|
|1. (ec (f631165 c637951 c637950 Var32) c637951)
|2. (~ (ntpp c637951 c637950))
|3. (~ (tpp c637951 c637950))
|4. (pp c637951 c637950)
|
|> ((ec (f631165 Y Z X) Z) <-- (~ (ntpp Y Z)) (pp Y Z))
||=============================
||Step 8
||
||? (~ (ntpp c637951 c637950))
||
||1. (~ (ec (f631165 c637951 c637950 Var32) c637950))
||2. (ec (f631165 c637951 c637950 Var32) c637951)
||3. (~ (ntpp c637951 c637950))
||4. (~ (tpp c637951 c637950))
||5. (pp c637951 c637950)
||
||> hyp
|=============================
|Step 9
|
|? (pp c637951 c637950)
|
|1. (~ (ec (f631165 c637951 c637950 Var32) c637950))
|2. (ec (f631165 c637951 c637950 Var32) c637951)
|3. (~ (ntpp c637951 c637950))
|4. (~ (tpp c637951 c637950))
|5. (pp c637951 c637950)
|
|> hyp
=============================
Step 10

? (~ (tpp c637951 c637950))

1. (ec (f631165 c637951 c637950 Var32) c637951)
2. (~ (ntpp c637951 c637950))
3. (~ (tpp c637951 c637950))
4. (pp c637951 c637950)

> hyp


LEMMA

Refine the overlap case from po or pp to po or tpp or ntpp.
=============================
Step 1

? (all x (all y (all z (((((dc x y) & (ntpp y z)) & (c x z)) & (o x z)) => ((po x z) v ((tpp x z) v (ntpp x z)))))))


> revsk
=============================
Step 2

? (((((~ (dc c645007 c645006)) v (~ (ntpp c645006 c645005))) v (~ (c c645007 c645005))) v (~ (o c645007 c645005))) v ((po c645007 c645005) v ((tpp c645007 c645005) v (ntpp c645007 c645005))))


> hypdisj
=============================
Step 3

? (ntpp c645007 c645005)

1. (~ (tpp c645007 c645005))
2. (~ (po c645007 c645005))
3. (o c645007 c645005)
4. (c c645007 c645005)
5. (ntpp c645006 c645005)
6. (dc c645007 c645006)

> ((ntpp X Y) <-- (pp X Y) (~ (tpp X Y)))
|=============================
|Step 4
|
|? (pp c645007 c645005)
|
|1. (~ (ntpp c645007 c645005))
|2. (~ (tpp c645007 c645005))
|3. (~ (po c645007 c645005))
|4. (o c645007 c645005)
|5. (c c645007 c645005)
|6. (ntpp c645006 c645005)
|7. (dc c645007 c645006)
|
|> ((pp Y Z) <-- (dc Y X) (ntpp X Z) (c Y Z) (o Y Z) (~ (po Y Z)))
|||||=============================
|||||Step 5
|||||
|||||? (dc c645007 Var32)
|||||
|||||1. (~ (pp c645007 c645005))
|||||2. (~ (ntpp c645007 c645005))
|||||3. (~ (tpp c645007 c645005))
|||||4. (~ (po c645007 c645005))
|||||5. (o c645007 c645005)
|||||6. (c c645007 c645005)
|||||7. (ntpp c645006 c645005)
|||||8. (dc c645007 c645006)
|||||
|||||> hyp
||||=============================
||||Step 6
||||
||||? (ntpp c645006 c645005)
||||
||||1. (~ (pp c645007 c645005))
||||2. (~ (ntpp c645007 c645005))
||||3. (~ (tpp c645007 c645005))
||||4. (~ (po c645007 c645005))
||||5. (o c645007 c645005)
||||6. (c c645007 c645005)
||||7. (ntpp c645006 c645005)
||||8. (dc c645007 c645006)
||||
||||> hyp
|||=============================
|||Step 7
|||
|||? (c c645007 c645005)
|||
|||1. (~ (pp c645007 c645005))
|||2. (~ (ntpp c645007 c645005))
|||3. (~ (tpp c645007 c645005))
|||4. (~ (po c645007 c645005))
|||5. (o c645007 c645005)
|||6. (c c645007 c645005)
|||7. (ntpp c645006 c645005)
|||8. (dc c645007 c645006)
|||
|||> hyp
||=============================
||Step 8
||
||? (o c645007 c645005)
||
||1. (~ (pp c645007 c645005))
||2. (~ (ntpp c645007 c645005))
||3. (~ (tpp c645007 c645005))
||4. (~ (po c645007 c645005))
||5. (o c645007 c645005)
||6. (c c645007 c645005)
||7. (ntpp c645006 c645005)
||8. (dc c645007 c645006)
||
||> hyp
|=============================
|Step 9
|
|? (~ (po c645007 c645005))
|
|1. (~ (pp c645007 c645005))
|2. (~ (ntpp c645007 c645005))
|3. (~ (tpp c645007 c645005))
|4. (~ (po c645007 c645005))
|5. (o c645007 c645005)
|6. (c c645007 c645005)
|7. (ntpp c645006 c645005)
|8. (dc c645007 c645006)
|
|> hyp
=============================
Step 10

? (~ (tpp c645007 c645005))

1. (~ (ntpp c645007 c645005))
2. (~ (tpp c645007 c645005))
3. (~ (po c645007 c645005))
4. (o c645007 c645005)
5. (c c645007 c645005)
6. (ntpp c645006 c645005)
7. (dc c645007 c645006)

> hyp


LEMMA

Combine the same local case splits as before.
=============================
Step 1

? (all x (all y (all z (((dc x y) & (ntpp y z)) => (((((dc x z) v (ec x z)) v (po x z)) v (tpp x z)) v (ntpp x z))))))


> revsk
=============================
Step 2

? (((~ (dc c652923 c652922)) v (~ (ntpp c652922 c652921))) v (((((dc c652923 c652921) v (ec c652923 c652921)) v (po c652923 c652921)) v (tpp c652923 c652921)) v (ntpp c652923 c652921)))


> hypdisj
=============================
Step 3

? (ntpp c652923 c652921)

1. (~ (tpp c652923 c652921))
2. (~ (po c652923 c652921))
3. (~ (ec c652923 c652921))
4. (~ (dc c652923 c652921))
5. (ntpp c652922 c652921)
6. (dc c652923 c652922)

> ((ntpp Y Z) <-- (dc Y X) (ntpp X Z) (c Y Z) (o Y Z) (~ (po Y Z)) (~ (tpp Y Z)))
|||||=============================
|||||Step 4
|||||
|||||? (dc c652923 Var35)
|||||
|||||1. (~ (ntpp c652923 c652921))
|||||2. (~ (tpp c652923 c652921))
|||||3. (~ (po c652923 c652921))
|||||4. (~ (ec c652923 c652921))
|||||5. (~ (dc c652923 c652921))
|||||6. (ntpp c652922 c652921)
|||||7. (dc c652923 c652922)
|||||
|||||> hyp
||||=============================
||||Step 5
||||
||||? (ntpp c652922 c652921)
||||
||||1. (~ (ntpp c652923 c652921))
||||2. (~ (tpp c652923 c652921))
||||3. (~ (po c652923 c652921))
||||4. (~ (ec c652923 c652921))
||||5. (~ (dc c652923 c652921))
||||6. (ntpp c652922 c652921)
||||7. (dc c652923 c652922)
||||
||||> hyp
|||=============================
|||Step 6
|||
|||? (c c652923 c652921)
|||
|||1. (~ (ntpp c652923 c652921))
|||2. (~ (tpp c652923 c652921))
|||3. (~ (po c652923 c652921))
|||4. (~ (ec c652923 c652921))
|||5. (~ (dc c652923 c652921))
|||6. (ntpp c652922 c652921)
|||7. (dc c652923 c652922)
|||
|||> ((c X Y) <-- (~ (dc X Y)))
|||=============================
|||Step 7
|||
|||? (~ (dc c652923 c652921))
|||
|||1. (~ (c c652923 c652921))
|||2. (~ (ntpp c652923 c652921))
|||3. (~ (tpp c652923 c652921))
|||4. (~ (po c652923 c652921))
|||5. (~ (ec c652923 c652921))
|||6. (~ (dc c652923 c652921))
|||7. (ntpp c652922 c652921)
|||8. (dc c652923 c652922)
|||
|||> hyp
||=============================
||Step 8
||
||? (o c652923 c652921)
||
||1. (~ (ntpp c652923 c652921))
||2. (~ (tpp c652923 c652921))
||3. (~ (po c652923 c652921))
||4. (~ (ec c652923 c652921))
||5. (~ (dc c652923 c652921))
||6. (ntpp c652922 c652921)
||7. (dc c652923 c652922)
||
||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|||=============================
|||Step 9
|||
|||? (c c652923 c652921)
|||
|||1. (~ (o c652923 c652921))
|||2. (~ (ntpp c652923 c652921))
|||3. (~ (tpp c652923 c652921))
|||4. (~ (po c652923 c652921))
|||5. (~ (ec c652923 c652921))
|||6. (~ (dc c652923 c652921))
|||7. (ntpp c652922 c652921)
|||8. (dc c652923 c652922)
|||
|||> ((c X Y) <-- (~ (dc X Y)))
|||=============================
|||Step 10
|||
|||? (~ (dc c652923 c652921))
|||
|||1. (~ (c c652923 c652921))
|||2. (~ (o c652923 c652921))
|||3. (~ (ntpp c652923 c652921))
|||4. (~ (tpp c652923 c652921))
|||5. (~ (po c652923 c652921))
|||6. (~ (ec c652923 c652921))
|||7. (~ (dc c652923 c652921))
|||8. (ntpp c652922 c652921)
|||9. (dc c652923 c652922)
|||
|||> hyp
||=============================
||Step 11
||
||? (~ (ec c652923 c652921))
||
||1. (~ (o c652923 c652921))
||2. (~ (ntpp c652923 c652921))
||3. (~ (tpp c652923 c652921))
||4. (~ (po c652923 c652921))
||5. (~ (ec c652923 c652921))
||6. (~ (dc c652923 c652921))
||7. (ntpp c652922 c652921)
||8. (dc c652923 c652922)
||
||> hyp
|=============================
|Step 12
|
|? (~ (po c652923 c652921))
|
|1. (~ (ntpp c652923 c652921))
|2. (~ (tpp c652923 c652921))
|3. (~ (po c652923 c652921))
|4. (~ (ec c652923 c652921))
|5. (~ (dc c652923 c652921))
|6. (ntpp c652922 c652921)
|7. (dc c652923 c652922)
|
|> hyp
=============================
Step 13

? (~ (tpp c652923 c652921))

1. (~ (ntpp c652923 c652921))
2. (~ (tpp c652923 c652921))
3. (~ (po c652923 c652921))
4. (~ (ec c652923 c652921))
5. (~ (dc c652923 c652921))
6. (ntpp c652922 c652921)
7. (dc c652923 c652922)

> hyp
